P:(chain_config()).
P(cchead())
 P(cctail())
 (id:Id. P(ccpred(id)))
 (id:Id, num:. P(ccsucc(id;num)))
 {x:chain_config(). P(x)} 

latex

Definitions	t  T, f(a), x(s), x:AB(x), x:A. B(x), Id, , ccpred(id), ccsucc(id;num), cctail(), s = t, cchead(), x:A  B(x), left + right, , Unit, chain_config(), {T}, Type, , Void, strong-subtype(A;B), P  Q
Lemmas	nat wf, Id wf, guard wf, chain config wf